Nuprl Lemma : l_contains_disjoint
11,40
postcript
pdf
T
:Type,
A
,
B
,
C
:(
T
List).
B
A
l_disjoint(
T
;
A
;
C
)
l_disjoint(
T
;
B
;
C
)
latex
Definitions
A
B
,
l_disjoint(
T
;
l1
;
l2
)
,
x
L
.
P
(
x
)
,
,
A
,
False
,
(
x
l
)
,
P
&
Q
,
x
:
A
.
B
(
x
)
,
P
Q
,
t
T
Lemmas
l
member
wf
,
not
wf
origin
T:Type, A, B, C:(T List). B 
A 
l_disjoint(T;A;C) l_disjoint(T;B;C) T:Type, A, B, C:(T List). B A l_disjoint(T;A;C) l_disjoint(T;B;C) Bx
L. P(x)
A l)x:A. B(x) Q T